The application of formal verification techniques, such as model checking, to real-life industrial designs, has traditionally been hampered by what is commonly known as the state explosion problem. Dramatic increases in the size of digital systems and components and the corresponding exponential increase in the size of their state space have kept industrial-size designs well beyond the capacity of current model checkers. “Abstraction refinement” has recently emerged as a promising technology that has the potential to bridge this verification gap.
The basic idea behind abstraction refinement is to attempt to verify the property at hand on a simplified version of the given design. This simplified version, or “abstraction,” is generated by removing elements from the original design that are not relevant to the proof of the given property. If the property passes on the abstract model it is guaranteed to be true on the original design as well. However, if the property fails, counter-examples produced on the abstract model must be validated against the original design. If this is not possible, the process is iterated with another abstract model which approximates the original model more closely. The new abstract model can be obtained by embellishing the current abstraction with more details from the original design or by re-generating a more complete abstract model from the original design. Usually the challenge in abstraction refinement is to construct as small an abstract model as possible, to facilitate the model checking, while retaining sufficient detail in the abstraction to decide the property. Thus, the ideal technique for abstraction refinement is one which achieves a good balance between the size and accuracy of the abstract model.
Abstraction refinement methods can be broadly classified into two kinds of methods, namely (1) counter-example driven and (2) counter-example independent. Counter-example driven methods for abstraction refinement typically work by iteratively refining the current abstraction so as to block a particular (false) counter-example encountered in model checking the previous abstract model. The refinement algorithm could use a combination of structural heuristics or functional analysis based on SAT or BDDs or some combination of these. Some recent techniques have enlarged the scope of the refinement by using multiple counter-examples from the previous abstract model.
The basic idea of counter-example independent abstraction refinement is to perform a SAT-based bounded model check (BMC) of the property up to some depth, k, on the original design and generate the abstract model through an analysis of the proof of unsatisfiability of the BMC problem. Essentially, the abstraction excludes latches and/or gates that are not included in the proof of unsatisfiability of the BMC problem and thereby guarantees that the abstract model also does not have any counter-examples up to depth k. Successive abstract models are similarly generated by solving BMC problems of increasing depth.